(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(x, c(x), c(y)) → f(y, y, f(y, x, y))
f(s(x), y, z) → f(x, s(c(y)), c(z))
f(c(x), x, y) → c(y)
g(x, y) → x
g(x, y) → y

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c3, c4, c5

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing nodes:

G(z0, z1) → c5
G(z0, z1) → c4
F(c(z0), z0, z1) → c3

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

g(z0, z1) → z0
g(z0, z1) → z1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1)) by

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c1

(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

(15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
We considered the (Usable) Rules:none
And the Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1, x2, x3)) = [2]x2   
POL(c(x1)) = [1] + x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(f(x1, x2, x3)) = 0   
POL(s(x1)) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2))) by

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0))))) by

F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

(25) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0))) by

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1))) by

F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c1

(29) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2))) by

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
S tuples:

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
K tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(31) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
S tuples:

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
K tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(33) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0))))))) by

F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
S tuples:

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
K tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(35) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
We considered the (Usable) Rules:none
And the Tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1, x2, x3)) = [2]x1 + x2   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(f(x1, x2, x3)) = 0   
POL(s(x1)) = [1] + x1   

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(x0))), c(c(s(s(x0)))), c(s(s(x0)))) → c3(F(s(s(x0)), s(s(x0)), f(x0, s(c(s(c(c(s(s(x0))))))), c(c(s(s(x0)))))))
S tuples:none
K tuples:

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(c(c(c(y0))), c(c(c(c(y0)))), c(c(c(y0)))) → c1(F(c(c(y0)), c(c(c(y0))), c(c(y0))))
F(c(c(s(s(y2)))), c(c(c(s(s(y2))))), c(c(s(s(y2))))) → c1(F(c(s(s(y2))), c(c(s(s(y2)))), c(s(s(y2)))))
F(c(c(s(y0))), c(c(c(s(y0)))), c(c(s(y0)))) → c1(F(c(s(y0)), c(c(s(y0))), c(s(y0))))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(37) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(38) BOUNDS(1, 1)